检索结果

Select

1. 基于随机障碍验证的随机连续系统安全性验证

沈敏捷, 曾振柄, 林望, 杨争峰

计算机应用 2018, 38 (6): 1737-1744. DOI: 10.11772/j.issn.1001-9081.2017112824

摘要（441）

PDF （1360KB）（300）

针对一类同时具有随机初始状态和随机微分方程的随机连续系统的安全性验证问题，提出一种基于随机障碍验证以及初始集选择的计算方法。首先，介绍了随机连续系统及其安全性验证的相关知识及概念；然后，讨论了如何对于服从几种不同分布的初始变量确定初始状态集，并根据选定的初始状态集使用随机障碍验证的方法将安全性验证问题转化为多项式优化问题；最后，运用平方和松弛方法将问题转化为平方和规划问题，并利用SOSTOOLS工具求得安全性概率的下界。理论分析以及实验结果表明，所提方法具有多项式时间的复杂度，能有效地给出随机连续系统在无界时间内的安全性概率的下界。

参考文献 | 相关文章 | 多维度评价

Select

2. 改进的几何定理机器证明的概率性算法

陈明雁曾振柄

计算机应用 2014, 34 (7): 2080-2084. DOI: 10.11772/j.issn.1001-9081.2014.07.2080

摘要（263）

PDF （835KB）（540）

将几何定理机器证明的研究方法概括为确定性算法与概率性算法两大类，针对已有的确定性算法和概率性算法的证明速率偏低或占用内存过大等问题，提出一种改进的概率性算法。主要是在改进对多项式中独立变元次数的上界估计的算法的基础上，结合Schwartz-Zippel定理和统计学理论，通过随机检验若干实例来证明几何定理，并能控制证明结果不真的概率在给定的小范围内。通过改进的概率性算法，成功在2秒内证明出代数法难以证明的五圆定理。最后的多组对比实验进一步表明，改进的概率性算法具有明显高效性。

参考文献 | 相关文章 | 多维度评价

Select

3. 基于多面体包含的非线性混成系统可达性分析

邹进林望罗勇曾振柄

计算机应用 2013, 33 (05): 1289-1293. DOI: 10.3724/SP.J.1087.2013.01289

摘要（771）

PDF （732KB）（554）

针对一类非线性混成系统的可达性问题，提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性，讨论了如何应用多面体包含对多项式混成系统进行线性近似，并采用量词消去和非线性优化方法来构造相应的线性混成系统，然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集，并应用于验证系统的安全性。

参考文献 | 相关文章 | 多维度评价

Select

4. 一阶子句搜索方法

郭远华曾振柄

计算机应用 2009, 29 (11): 3064-3067.

摘要（1133）

PDF （693KB）（1115）

子句集的可满足性判定是自动证明领域的热点之一。提出了子句搜索方法判定命题子句集Φ的可满足性，该方法查找Φ中子句的一个公共不可扩展子句C，当且仅当找到C时Φ可满足，此时C中各文字的补构成一个模型。结合部分实例化方法将子句搜索方法提升至一阶。一阶子句搜索方法可以判定子句集的M可满足性，具备终止性、正确性和完备性，是一种判定子句集可满足性的有效方法。

相关文章 | 多维度评价

Select

5. 非线性循环不变式的自动生成

毕忠勤曾振柄郭远华

计算机应用

摘要（1359）

PDF （608KB）（902）

提出了一个自动生成非线性循环不变式的算法。循环不变式可以表示成一个带参数的多项式的形式，根据断言的归纳特性，将循环不变式的生成问题转变成一个约束求解问题，这个约束求解问题的每个解对应于一个循环不变式，如果约束求解问题仅有零解，则说明不存在该参数多项式形式的循环不变式。该算法在Maple中得到了实现，并通过一些实例说明了该算法的有效性。

相关文章 | 多维度评价

Select

6. 基于动态几何技术的平面几何资源库检索

郭远华曾振柄毕忠勤郭远刚

计算机应用

摘要（1838）

PDF （428KB）（966）

在几何资源库中使用传统的方法检索相似的几何题，效果并不理想。对于基于动态几何技术的平面几何资源库，提出使用几何特征量进行相似性检索的方法。几何特征量量化了几何命题中的各几何元素，可以由动态几何作图指令序列提取，该方法能较好地检索相似的几何命题。

相关文章 | 多维度评价

Select

7. 基于AJAX和自动推理技术构建交互式数学Web服务

曾振柄陈良育张骏符红光

计算机应用

摘要（1715）

PDF （796KB）（1217）

数学辅助学习平台一直是数学教育和计算机领域的研究热点。传统设计方法在教学互动、智能教育和界面友好性等环节存在若干制约因素。集成领先的AJAX思想和成熟的自动推理算法，提出新的数学Web服务系统设计方法，辅以MathML数学表示语言等多项先进技术，构建一个交互式数学Web服务学习平台。实际运行结果表明，平台具有良好的表现形式和运行性能，为使用者提供一个良好的交互式学习环境。

相关文章 | 多维度评价

Select

8. 寻找平面代数剖分样本点的改进算法

单美静曾振柄毕忠勤

计算机应用

摘要（1391）

PDF （487KB）（846）

基于非线性多项式方程的零点配对算法以及临界点算法，给出了一种求平面代数剖分样本点的改进算法。该算法剔除了大量冗余样本点，并在计算过程中以区间表示代数数，有效避免了浮点数等近似计算。通过与已有的经典算法进行比较，实验结果表明该算法具有显著的效果。

相关文章 | 多维度评价

Select

9. 一种混合高性能计算机代数环境模型

张骏陈良育曾振柄

计算机应用

摘要（1460）

提出一种高性能计算机代数环境HHPCAS，综合现有的多种计算机代数软件，通过添加内核扩展函数、外部调用等方法，结合集群管理软件和并行环境，可以提供高性能的计算机代数计算环境。HHPCAS根据Slot/Ticket模型可以有效管理可用计算资源和作业优先等级，充分发挥多种计算机代数软件的特长，并且提供并行的消息传递机制，将大量复杂的计算平均分配到每个计算节点，解决单台机器内存受限和计算能力有限等问题。通过并行差分代换方法测试表明HHPCAS可以为符号计算和计算机自动推理提供有效的计算平台。

相关文章 | 多维度评价

Select

10. 基于小波的压缩图像索引技术

张问银;曾振柄

计算机应用

摘要（1692）

PDF （387KB）（679）

在JPEG2000压缩框架下给出了两种压缩图像索引方法, 不需要完全解压缩, 减少了数据处理量。实验结果证明，给出的索引方法具有很强的图像表征能力，利用该索引进行图像检索,提高了检索效率。

相关文章 | 多维度评价

Select

11. 基于图形理解的汉字构形自动分析系统

陈良育，曾振柄，张问银

计算机应用 2005, 25 (07): 1629-1631. DOI: 10.3724/SP.J.1087.2005.01629

摘要（1316）

PDF （473KB）（725）

汉字构形自动分析系统将计算机视觉，图像理解等领域中业已成熟的诸多技术，应用到汉字构形学研究的各主要环节。以GB231280汉字集合所生成的构件图片为基础对象，生成了汉字部件构形描述，有效率达90%以上。

参考文献 | 相关文章 | 多维度评价